(set-info :smt-lib-version 2.6)
(set-logic QF_BV)
(set-info :source |
 Patrice Godefroid, SAGE (systematic dynamic test generation)
 For more information: http://research.microsoft.com/en-us/um/people/pg/public_psfiles/ndss2008.pdf
|)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun T4_10728 () (_ BitVec 32))
(declare-fun T4_4601 () (_ BitVec 32))
(declare-fun T1_10728 () (_ BitVec 8))
(declare-fun T1_10729 () (_ BitVec 8))
(declare-fun T1_10730 () (_ BitVec 8))
(declare-fun T1_10731 () (_ BitVec 8))
(declare-fun T1_4601 () (_ BitVec 8))
(declare-fun T1_4602 () (_ BitVec 8))
(declare-fun T1_4603 () (_ BitVec 8))
(declare-fun T1_4604 () (_ BitVec 8))
(assert (and true (= T4_4601 (bvor (bvshl (bvor (bvshl (bvor (bvshl ((_ zero_extend 24) T1_4604) (_ bv8 32)) ((_ zero_extend 24) T1_4603)) (_ bv8 32)) ((_ zero_extend 24) T1_4602)) (_ bv8 32)) ((_ zero_extend 24) T1_4601))) (= T4_10728 (bvor (bvshl (bvor (bvshl (bvor (bvshl ((_ zero_extend 24) T1_10731) (_ bv8 32)) ((_ zero_extend 24) T1_10730)) (_ bv8 32)) ((_ zero_extend 24) T1_10729)) (_ bv8 32)) ((_ zero_extend 24) T1_10728))) (bvslt (bvadd T4_10728 (_ bv15 32)) (_ bv0 32)) (not (= T4_4601 (_ bv4294967295 32))) (bvule T4_10728 (_ bv2147483647 32)) (bvult T4_10728 (_ bv4294967295 32)) (= T4_4601 T4_10728) (not (= T4_10728 (_ bv0 32)))))
(check-sat)
(exit)
